{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}

module AnonymousFunctions where

import TypeBasics (encode)
import TypeSums (inject)
import Yoko

import Common



data AnonTerm = Lam Type AnonTerm | Var Int
              | Let [Decl] AnonTerm
              | App AnonTerm AnonTerm deriving Show

data Decl = Decl Type AnonTerm deriving Show


data Lam_ = Lam_ Type AnonTerm
data Var_ = Var_ Int
data Let_ = Let_ [Decl] AnonTerm
data App_ = App_ AnonTerm AnonTerm

data Decl_ = Decl_ Type AnonTerm



type instance Range Lam_ = AnonTerm
type instance Range Var_ = AnonTerm
type instance Range Let_ = AnonTerm
type instance Range App_ = AnonTerm

type instance Range Decl_ = Decl

type instance Tag Lam_ = $(return $ encode "Lam")
type instance Tag Var_ = $(return $ encode "Var")
type instance Tag Let_ = $(return $ encode "Let")
type instance Tag App_ = $(return $ encode "App")

type instance Tag Decl_ = $(return $ encode "Decl")

concat `fmap` mapM derive [''AnonTerm, ''Decl, ''Lam_, ''Var_, ''Let_, ''App_, ''Decl_]



type instance Rep Lam_ = Dep Type :*: Rec AnonTerm
instance Generic Lam_ where
  rep (Lam_ ty tm) = Dep ty :*: Rec tm
  obj (Dep ty :*: Rec tm) = Lam_ ty tm
type instance Rep Var_ = Dep Int
instance Generic Var_ where
  rep (Var_ i) = Dep i
  obj (Dep i) = Var_ i
type instance Rep Let_ = Par1 [] (Rec Decl) :*: Rec AnonTerm
instance Generic Let_ where
  rep (Let_ ds tm) = Par1 (map Rec ds) :*: Rec tm
  obj (Par1 ds :*: Rec tm) = Let_ (fmap unRec ds) tm
type instance Rep App_ = Rec AnonTerm :*: Rec AnonTerm
instance Generic App_ where
  rep (App_ tm1 tm2) = Rec tm1 :*: Rec tm2
  obj (Rec tm1 :*: Rec tm2) = App_ tm1 tm2

type instance Rep Decl_ = Dep Type :*: Rec AnonTerm
instance Generic Decl_ where
  rep (Decl_ ty tm) = Dep ty :*: Rec tm
  obj (Dep ty :*: Rec tm) = Decl_ ty tm



type instance DCs AnonTerm =
  (N Lam_ :+: N Var_) :+: (N Let_ :+: N App_)
instance DT AnonTerm where
  disband (Lam ty tm)   = DCsOf . inject $ Lam_ ty tm
  disband (Var i)       = DCsOf . inject $ Var_ i
  disband (Let ds tm)   = DCsOf . inject $ Let_ ds tm
  disband (App tm1 tm2) = DCsOf . inject $ App_ tm1 tm2
instance DC Lam_ where rejoin (Lam_ ty tm)   = Lam ty tm
instance DC Var_ where rejoin (Var_ i)       = Var i
instance DC Let_ where rejoin (Let_ ds tm)   = Let ds tm
instance DC App_ where rejoin (App_ tm1 tm2) = App tm1 tm2

type instance DCs Decl = N Decl_
instance DT Decl where
  disband (Decl ty tm) = DCsOf . N $ Decl_ ty tm
instance DC Decl_ where rejoin (Decl_ ty tm) = Decl ty tm
